Nuprl Lemma : Id_sq 0,22
SQType(Id) 
latex

DefinitionsId, SQType(T), x:A. B(x), P  Q, t  T, Prop

origin